Multiparty session types are a type system that can ensure the safety andliveness of distributed peers via the global specification of theirinteractions. To construct a global specification from a set of distributeduncontrolled behaviours, this paper explores the problem of fullycharacterising multiparty session types in terms of communicating automata. Weequip global and local session types with labelled transition systems (LTSs)that faithfully represent asynchronous communications through unboundedbuffered channels. Using the equivalence between the two LTSs, we identify aclass of communicating automata that exactly correspond to the projected localtypes. We exhibit an algorithm to synthesise a global type from a collection ofcommunicating automata. The key property of our findings is the notion ofmultiparty compatibility which non-trivially extends the duality condition forbinary session types.
展开▼
